CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM];

EDIT-STRATEGY-IS: 
DEPTH[2]∨LENGTH[2];

ELAPSED-TIME =2817

NIL 1 4
1 ¬P(x,G21(y));3 4
3 ¬(P(z,x)∧P(x,y));5 6
4 P(G21(x),x);G2
5 ¬G(x,y);THM
6 P(x,z)∧P(z,y)⊃G(x,y);G1